approx_sm(es; In; Out; Cmd; isupdate; Rsp; Delta; Q)
== expl:E(Out)({e:E(In)| (isupdate(In(e)))}  List)
== ((e:E(Out).
== (((e':E(In). (e'  expl(e))  e' c e) & ((is-query(In;isupdate;e))  ((null(expl(e))))))
== & (e1, e2:E(Out). expl(e1)  expl(e2)  expl(e2)  expl(e1))
== & (e:E(Out).
== & ((is-query(In;isupdate;e)  (Out(e) = Q(In(expl(e)),In(e))))
== & (& ((is-query(In;isupdate;e))  (Out(e) = Delta(In(expl(e))))))) 

latex

---

clarification:

approx_sm(es; In; Out; Cmd; isupdate; Rsp; Delta; Q)
== expl:es-E-interface(es;Out)({e:es-E-interface(es;In)| (isupdate(In(e)))}  List)
== ((e:es-E-interface(es;Out).
== (((e':es-E-interface(es;In). (e'  expl(e)  es-E-interface(es;In))  es-causle(es;e';e))
== ((& ((is-query(In;isupdate;e))  ((null(expl(e))))))
== & (e1:es-E-interface(es;Out), e2:es-E-interface(es;Out).
== & (expl(e1)  expl(e2)  es-E-interface(es;In) List
== & ( expl(e2)  expl(e1)  es-E-interface(es;In) List)
== & (e:es-E-interface(es;Out).
== & ((is-query(In;isupdate;e)  (Out(e) = Q(In(expl(e)),In(e))  Rsp))
== & (& ((is-query(In;isupdate;e))  (Out(e) = Delta(In(expl(e)))  Rsp)))) 

latex

Up	abstract chain replication
Wellformedness Lemmas	approx sm wf
Definitions	x:A. B(x), x:AB(x), type List, {x:A| B(x)} , (x  l), e c e', b, null(as), P  Q, l1  l2, x:A. B(x), E(X), P & Q, P  Q, A, is-query(In;isupdate;e), s = t, X(e), X(L), f(a)